//
// THIS FILE IS AUTOMATICALLY GENERATED!!
//
// Generated at Thu 06-Dec-2012 by the VDM++ to JAVA Code Generator
// (v8.0 - Mon 09-Jul-2007 09:32:40)
//
// Supported compilers:
// jdk1.4
//

// ***** VDMTOOLS START Name=HeaderComment KEEP=NO
// ***** VDMTOOLS END Name=HeaderComment

// ***** VDMTOOLS START Name=package KEEP=NO
// ***** VDMTOOLS END Name=package

// ***** VDMTOOLS START Name=imports KEEP=NO

import jp.co.csk.vdm.toolbox.VDM.*;
import java.util.*;
import jp.co.csk.vdm.toolbox.VDM.jdk.*;
// ***** VDMTOOLS END Name=imports



public class Test implements EvaluatePP {

// ***** VDMTOOLS START Name=vdmComp KEEP=NO
  static UTIL.VDMCompare vdmComp = new UTIL.VDMCompare();
// ***** VDMTOOLS END Name=vdmComp

// ***** VDMTOOLS START Name=uml KEEP=NO
  public volatile UML uml = null;
// ***** VDMTOOLS END Name=uml

// ***** VDMTOOLS START Name=q1 KEEP=NO
  private volatile State q1 = null;
// ***** VDMTOOLS END Name=q1

// ***** VDMTOOLS START Name=q2 KEEP=NO
  private volatile State q2 = null;
// ***** VDMTOOLS END Name=q2

// ***** VDMTOOLS START Name=q3 KEEP=NO
  private volatile State q3 = null;
// ***** VDMTOOLS END Name=q3

// ***** VDMTOOLS START Name=q4 KEEP=NO
  private volatile State q4 = null;
// ***** VDMTOOLS END Name=q4

// ***** VDMTOOLS START Name=q5 KEEP=NO
  private volatile State q5 = null;
// ***** VDMTOOLS END Name=q5

// ***** VDMTOOLS START Name=t1 KEEP=NO
  private volatile Transition t1 = null;
// ***** VDMTOOLS END Name=t1

// ***** VDMTOOLS START Name=t2 KEEP=NO
  private volatile Transition t2 = null;
// ***** VDMTOOLS END Name=t2

// ***** VDMTOOLS START Name=t3 KEEP=NO
  private volatile Transition t3 = null;
// ***** VDMTOOLS END Name=t3

// ***** VDMTOOLS START Name=t4 KEEP=NO
  private volatile Transition t4 = null;
// ***** VDMTOOLS END Name=t4

// ***** VDMTOOLS START Name=t5 KEEP=NO
  private volatile Transition t5 = null;
// ***** VDMTOOLS END Name=t5

// ***** VDMTOOLS START Name=t6 KEEP=NO
  private volatile Transition t6 = null;
// ***** VDMTOOLS END Name=t6

// ***** VDMTOOLS START Name=sentinel KEEP=NO
  volatile Sentinel sentinel;
// ***** VDMTOOLS END Name=sentinel


// ***** VDMTOOLS START Name=TestSentinel KEEP=NO
  class TestSentinel extends Sentinel {

    public final int Run = 0;

    public final int Test = 1;

    public final int getState = 2;

    public final int findState = 3;

    public final int checkEmpty = 4;

    public final int initialize = 5;

    public final int testaTrace = 6;

    public final int runSmallSeq = 7;

    public final int getAllStates = 8;

    public final int findStateName = 9;

    public final int testaWrongTrace = 10;

    public final int howManySequences = 11;

    public final int testaCyclicTrace = 12;

    public final int getaTransitionName = 13;

    public final int nr_functions = 14;


    public TestSentinel () throws CGException {}


    public TestSentinel (EvaluatePP instance) throws CGException {
      init(nr_functions, instance);
    }

  }
// ***** VDMTOOLS END Name=TestSentinel
;

// ***** VDMTOOLS START Name=evaluatePP KEEP=NO
  public Boolean evaluatePP (int fnr) throws CGException {
    return new Boolean(true);
  }
// ***** VDMTOOLS END Name=evaluatePP


// ***** VDMTOOLS START Name=setSentinel KEEP=NO
  public void setSentinel () {
    try {
      sentinel = new TestSentinel(this);
    }
    catch (CGException e) {
      System.out.println(e.getMessage());
    }
  }
// ***** VDMTOOLS END Name=setSentinel


// ***** VDMTOOLS START Name=Test KEEP=NO
  public Test () throws CGException {

    try {

      setSentinel();
      q1 = (State) new State(new String("q1"));
      q2 = (State) new State(new String("q2"));
      q3 = (State) new State(new String("q3"));
      q4 = (State) new State(new String("q4"));
      q5 = (State) new State(new String("q5"));
      t1 = (Transition) new Transition(new String("t1"), q1, q2);
      t2 = (Transition) new Transition(new String("t2"), q2, q3);
      t3 = (Transition) new Transition(new String("t3"), q1, q4);
      t4 = (Transition) new Transition(new String("t4"), q4, q3);
      t5 = (Transition) new Transition(new String("t5"), q4, q1);
      t6 = (Transition) new Transition(new String("t6"), q3, q5);
    }
    catch (Exception e){

      e.printStackTrace(System.out);
      System.out.println(e.getMessage());
    }
    try {

      initialize();
      setSentinel();
    }
    catch (Throwable e) {
      System.out.println(e.getMessage());
    }
  }
// ***** VDMTOOLS END Name=Test


// ***** VDMTOOLS START Name=initialize KEEP=NO
  private void initialize () throws CGException {

    sentinel.entering(((TestSentinel) sentinel).initialize);
    try {

      q1.addTransition((Transition) t1);
      q2.addTransition((Transition) t2);
      q1.addTransition((Transition) t3);
      q4.addTransition((Transition) t4);
      q4.addTransition((Transition) t5);
      q3.addTransition((Transition) t6);
      UML rhs_13 = null;
      HashSet arg_15 = new HashSet();
      arg_15 = new HashSet();
      arg_15.add(q1);
      arg_15.add(q2);
      arg_15.add(q3);
      arg_15.add(q4);
      rhs_13 = new UML(q1, arg_15);
      uml = (UML) UTIL.clone(rhs_13);
    }
    finally {
      sentinel.leaving(((TestSentinel) sentinel).initialize);
    }
  }
// ***** VDMTOOLS END Name=initialize


// ***** VDMTOOLS START Name=Run KEEP=NO
  public HashSet Run (final Integer n) throws CGException {

    if (!this.pre_Run(n).booleanValue()) 
      UTIL.RunTime("Run-Time Error:Precondition failure in Run");
    sentinel.entering(((TestSentinel) sentinel).Run);
    try {

      HashSet rexpr_2 = new HashSet();
      rexpr_2 = uml.searchStart(n);
      return rexpr_2;
    }
    finally {
      sentinel.leaving(((TestSentinel) sentinel).Run);
    }
  }
// ***** VDMTOOLS END Name=Run


// ***** VDMTOOLS START Name=pre_Run KEEP=NO
  public Boolean pre_Run (final Integer n) throws CGException {
    return new Boolean((n.intValue()) > (new Integer(0).intValue()));
  }
// ***** VDMTOOLS END Name=pre_Run


// ***** VDMTOOLS START Name=runSmallSeq KEEP=NO
  public HashSet runSmallSeq (final Integer n) throws CGException {

    if (!this.pre_runSmallSeq(n).booleanValue()) 
      UTIL.RunTime("Run-Time Error:Precondition failure in runSmallSeq");
    sentinel.entering(((TestSentinel) sentinel).runSmallSeq);
    try {

      HashSet rexpr_2 = new HashSet();
      Object tmpGen_3 = null;
      State tmpRec_4 = null;
      tmpRec_4 = (State) uml.getStartState();
      {

        State obj_7 = null;
        obj_7 = (State) uml.getStartState();
        rexpr_2 = (HashSet) obj_7.search(n);
      }
      return rexpr_2;
    }
    finally {
      sentinel.leaving(((TestSentinel) sentinel).runSmallSeq);
    }
  }
// ***** VDMTOOLS END Name=runSmallSeq


// ***** VDMTOOLS START Name=pre_runSmallSeq KEEP=NO
  public Boolean pre_runSmallSeq (final Integer n) throws CGException {
    return new Boolean((n.intValue()) > (new Integer(0).intValue()));
  }
// ***** VDMTOOLS END Name=pre_runSmallSeq


// ***** VDMTOOLS START Name=howManySequences KEEP=NO
  public Integer howManySequences (final Integer n) throws CGException {

    if (!this.pre_howManySequences(n).booleanValue()) 
      UTIL.RunTime("Run-Time Error:Precondition failure in howManySequences");
    sentinel.entering(((TestSentinel) sentinel).howManySequences);
    try {

      Integer rexpr_2 = null;
      HashSet unArg_3 = new HashSet();
      unArg_3 = uml.searchStart(n);
      rexpr_2 = new Integer(unArg_3.size());
      return rexpr_2;
    }
    finally {
      sentinel.leaving(((TestSentinel) sentinel).howManySequences);
    }
  }
// ***** VDMTOOLS END Name=howManySequences


// ***** VDMTOOLS START Name=pre_howManySequences KEEP=NO
  public Boolean pre_howManySequences (final Integer n) throws CGException {
    return new Boolean((n.intValue()) > (new Integer(0).intValue()));
  }
// ***** VDMTOOLS END Name=pre_howManySequences


// ***** VDMTOOLS START Name=testaTrace KEEP=NO
  public Boolean testaTrace () throws CGException {

    sentinel.entering(((TestSentinel) sentinel).testaTrace);
    try {

      Boolean rexpr_1 = null;
      Vector par_2 = null;
      par_2 = new Vector();
      par_2.add(q1);
      par_2.add(q2);
      par_2.add(q3);
      rexpr_1 = uml.verifyPath(par_2);
      return rexpr_1;
    }
    finally {
      sentinel.leaving(((TestSentinel) sentinel).testaTrace);
    }
  }
// ***** VDMTOOLS END Name=testaTrace


// ***** VDMTOOLS START Name=testaWrongTrace KEEP=NO
  public Boolean testaWrongTrace () throws CGException {

    sentinel.entering(((TestSentinel) sentinel).testaWrongTrace);
    try {

      Boolean rexpr_1 = null;
      Vector par_2 = null;
      par_2 = new Vector();
      par_2.add(q1);
      par_2.add(q2);
      par_2.add(q3);
      par_2.add(q1);
      rexpr_1 = uml.verifyPath(par_2);
      return rexpr_1;
    }
    finally {
      sentinel.leaving(((TestSentinel) sentinel).testaWrongTrace);
    }
  }
// ***** VDMTOOLS END Name=testaWrongTrace


// ***** VDMTOOLS START Name=testaCyclicTrace KEEP=NO
  public Boolean testaCyclicTrace () throws CGException {

    sentinel.entering(((TestSentinel) sentinel).testaCyclicTrace);
    try {

      Boolean rexpr_1 = null;
      Vector par_2 = null;
      par_2 = new Vector();
      par_2.add(q1);
      par_2.add(q4);
      par_2.add(q1);
      par_2.add(q4);
      par_2.add(q1);
      par_2.add(q4);
      par_2.add(q1);
      par_2.add(q4);
      par_2.add(q3);
      rexpr_1 = uml.verifyPath(par_2);
      return rexpr_1;
    }
    finally {
      sentinel.leaving(((TestSentinel) sentinel).testaCyclicTrace);
    }
  }
// ***** VDMTOOLS END Name=testaCyclicTrace


// ***** VDMTOOLS START Name=getaTransitionName KEEP=NO
  public String getaTransitionName () throws CGException {

    sentinel.entering(((TestSentinel) sentinel).getaTransitionName);
    try {

      String rexpr_1 = null;
      rexpr_1 = t1.getName();
      return rexpr_1;
    }
    finally {
      sentinel.leaving(((TestSentinel) sentinel).getaTransitionName);
    }
  }
// ***** VDMTOOLS END Name=getaTransitionName


// ***** VDMTOOLS START Name=getAllStates KEEP=NO
  public HashMap getAllStates () throws CGException {

    sentinel.entering(((TestSentinel) sentinel).getAllStates);
    try {

      HashMap tmpObj_2 = new HashMap();
      tmpObj_2 = uml.states();
      return tmpObj_2;
    }
    finally {
      sentinel.leaving(((TestSentinel) sentinel).getAllStates);
    }
  }
// ***** VDMTOOLS END Name=getAllStates


// ***** VDMTOOLS START Name=findStateName KEEP=NO
  public Boolean findStateName (final String name) throws CGException {

    sentinel.entering(((TestSentinel) sentinel).findStateName);
    try {

      Boolean tmpObj_3 = null;
      tmpObj_3 = uml.stateExists(name);
      return tmpObj_3;
    }
    finally {
      sentinel.leaving(((TestSentinel) sentinel).findStateName);
    }
  }
// ***** VDMTOOLS END Name=findStateName


// ***** VDMTOOLS START Name=findState KEEP=NO
  public Boolean findState (final State state) throws CGException {

    sentinel.entering(((TestSentinel) sentinel).findState);
    try {

      Boolean tmpObj_3 = null;
      tmpObj_3 = uml.stateExists((State) state);
      return tmpObj_3;
    }
    finally {
      sentinel.leaving(((TestSentinel) sentinel).findState);
    }
  }
// ***** VDMTOOLS END Name=findState


// ***** VDMTOOLS START Name=checkEmpty KEEP=NO
  public Boolean checkEmpty () throws CGException {

    sentinel.entering(((TestSentinel) sentinel).checkEmpty);
    try {

      Boolean rexpr_1 = null;
      rexpr_1 = uml.isEmpty();
      return rexpr_1;
    }
    finally {
      sentinel.leaving(((TestSentinel) sentinel).checkEmpty);
    }
  }
// ***** VDMTOOLS END Name=checkEmpty


// ***** VDMTOOLS START Name=getState KEEP=NO
  public State getState (final String name) throws CGException {

    sentinel.entering(((TestSentinel) sentinel).getState);
    try {

      State rexpr_2 = null;
      rexpr_2 = (State) uml.getState(name);
      return (State) rexpr_2;
    }
    finally {
      sentinel.leaving(((TestSentinel) sentinel).getState);
    }
  }
// ***** VDMTOOLS END Name=getState

}
;
